ds:x:Id fp Type, da:k:Knd fp Type, a, b:msg-spec(ds;da). a  b  msg-spec(ds;da) 

latex

Definitions	Id, t  T, Type, x. t(x), x:A. B(x), a:A fp B(a), Knd, IdLnk, x:AB(x), x.A(x), 2of(t), 1of(t), msg-item(ds;da;k;l), type List, IdLnkDeq, KindDeq, product-deq(A;B;a;b), f  g, a  b, msg-spec(ds;da)
Lemmas	fpf-join wf, product-deq wf, Kind-deq wf, idlnk-deq wf, msg-item wf, pi1 wf, pi2 wf, IdLnk wf, Knd wf, fpf wf, Id wf